\documentclass[titlepage,12pt]{article}

\usepackage{ae,aecompl}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{epsfig}
\usepackage{color}
\usepackage{yhmath}
\usepackage{listings}
\usepackage{amsthm}
\usepackage{titling}
\usepackage{fancyhdr}

\pagestyle{fancy}
\lhead{DADDY v3.0} % texto izquierda de la cabecea
%\chead{} % texto centro de la cabecera
%\rhead{\thesection} % número de página a la derecha
\lfoot{User Manual} % texto izquierda del pie
\cfoot{} % imagen centro del pie
\rfoot{\thepage} % texto derecha del pie
%\renewcommand{\headrulewidth}{0.4pt} % Grosor de la línea del encabezado.
%\renewcommand{\footrulewidth}{0.4pt} % Grosor de la línea del pie de pagina.

\begin{document}

\begin{titlepage}
	\begin{flushright}
		\rule{110mm}{1mm}\\[0.25cm]
		\rule{130mm}{1mm}\\[1.5cm]
		{\Huge \textbf{DADDY v3.0 - User Manual}}\\[5cm]
	\end{flushright}
	\begin{center}
		{\Large \textbf{Diagnosability Analyzer for Distributed}}\\
		{\Large \textbf{Discrete sYstems}}\\[7cm]
	\end{center}
	\begin{flushright}
		Authors: \\
		Gonzalo Bonigo \\
		Hernan Ponce de Leon \\
		Laura Brand\'an Briones \\[0.25cm]
		\rule{130mm}{1mm}
	\end{flushright}
\end{titlepage}

\tableofcontents

\newpage

\section{Introduction}

DADDY is a command line application developed in Python that allows us to determine
 the diagnosability of concurrent and distributed systems in a compositional way.\\
\\
The program assumes that the system to be analyzed consists of subsystems working
in parallel, and try to decide the whole system diagnosability by analyzing its
subsystems or composition of them.\\
\\
It uses the \emph{twin-plant} method for deciding the diagnosability of the 
subsystems, and provides three different algorithms that use such method, where two
 of them try to improve it.\\
\\
Since subsystems are represented by Labelled Transition Systems, which are a class
of Finite State Machines, the application use a tool from the MCRL2 package, called
\emph{ltsgraph}, to representing them in a graphical way.

\newpage

\section{Requirements and Installation}

\subsection{Requirements}

\subsubsection{Python}

Since the application is a python script, you must have installed the python
interpreter: \\% You can download it from  its web site:\\

\emph{\textbf{http://www.python.org/download/}}\\
\\
DADDY was built and tested for the Python 2.7.3 version, but it should work well 
in all 2.7 releases:\\

\emph{\textbf{http://www.python.org/download/releases/2.7.3/}}\\
\\
If you run the application under other version, we give you no warranty about its
behavior.

\subsubsection{MCRL2}

DADDY use the tool \emph{\textbf{ltsgraph}} from the MCRL2 package to graphic the
systems:\\% You can download it from:\\

\emph{\textbf{http://www.mcrl2.org/release/user\_manual/download.html}}\\
\\
If you are under linux you can install it from a command line typing:\\

\texttt{sudo apt-get install mcrl2}\\
\\
or, if you are using pacman:\\

\texttt{sudo pacman -S mcrl2}\\
\\
The application was executed and tested for the MCRL2 201210.1 release, but it
should work in all releases that have the \emph{\textbf{ltsgraph}} tool.

\newpage

\subsection{Installation}

\subsubsection{Automatic Installation}

For an automatic installation run the \texttt{\textbf{install.py}} script within
the \texttt{\textbf{install}} directory.\\
\\
If you are under a \textbf{Linux} distribution run it as super user:\\

\texttt{\textbf{sudo python install.py}}\\
\\
If you are a \textbf{Windows Vista/7} user, you have to run it as administrator.
In all Windows systems you can run it by doing double click on the file, or
executing it in a command line (start the command line as administrator if you're
on Vista/7) by just typing:\\

\texttt{\textbf{python install.py}}

\subsubsection{Manual Installation}

If the automatic installation fails, you can try with a manual one.\\
\\
For a manual install, follow these steps depending on the operating system you are
using.\\
\\
\textbf{Linux:}\\
\\
1) You must open a terminal and go into the DADDY root directory. It looks like
this:\\
\\
\texttt{
daddy/\\
doc/\\
install/\\
license\\}
\\
2) Copy the \texttt{[daddy.py listpath.py sync.py]} files, within the
\texttt{daddy} directory, into the \texttt{/usr/bin/} directory, and give them
execution permission as follow:\\
\\

\texttt{sudo cp daddy/*.py /usr/bin/}

\texttt{sudo chmod 0777 /usr/bin/daddy.py}

\texttt{sudo chmod 0777 /usr/bin/listpath.py}

\texttt{sudo chmod 0777 /usr/bin/sync.py}\\
\\
3) Copy the \texttt{[lts]} and \texttt{[daddyparsers]} packages, within the
\texttt{daddy} directory, into the \texttt{site-packages} or \texttt{dist-packages}
directories from you python installation and give them the correct permission:\\

\texttt{sudo cp -r daddy/lts /usr/lib/python2.7/dist-packages/}

\texttt{sudo cp -r daddy/daddyparsers /usr/lib/python2.7/dist-packages/}

\texttt{sudo chmod 0777 /usr/lib/python2.7/dist-packages/lts}

\texttt{sudo chmod 0666 /usr/lib/python2.7/dist-packages/lts/*}

\texttt{sudo chmod 0777 /usr/lib/python2.7/dist-packages/lts/utils}

\texttt{sudo chmod 0666 /usr/lib/python2.7/dist-packages/lts/utils/*}

\texttt{sudo chmod 0777 /usr/lib/python2.7/dist-packages/daddyparsers}

\texttt{sudo chmod 0666 /usr/lib/python2.7/dist-packages/daddyparsers/*}\\
\\
4) Type \texttt{daddy.py -help} to check if it is well installed.\\
\\
\textbf{Windows:}\\
\\
1) You must open a command line or an explorer windows and go into the DADDY root
directory. It looks like this:\\
\\
\texttt{
daddy/\\
doc/\\
install/\\
license\\}
\\
2) Copy the \texttt{[daddy.py listpath.py sync.py]} files, within the
\texttt{daddy} directory, into the \texttt{C:/Python27/} directory:\\

\texttt{copy daddy/*.py C:/Python27/}\\
\\
3) Copy the \texttt{[lts]} and \texttt{[daddyparsers]} packages, within the
\texttt{daddy} directory, into the \texttt{site-packages} or \texttt{dist-packages}
directories from you python installation:\\

\texttt{copy daddy/lts c:/Python27/Lib/site-packages}

\texttt{copy daddy/daddyparsers c:/Python27/Lib/site-packages}\\
\\
4) Type \texttt{daddy.py -help} to check if it is well installed.

\subsubsection{No Installation}

There is still one more way to use DADDY, and that is without an installation.
You can actually use the application by appending the absolute path of the
\texttt{DADDY\_ROOT/daddy} directory to the system \texttt{PATH} variable.\\
\\
\textbf{Setting \texttt{PATH} variable on Linux}\\
\\
To set the PATH variable on Linux open the \texttt{.bash\_profile} or the
\texttt{.bashrc} file with a text editor and edit/add the line:\\
\\
\texttt{
\# User defined PATH.\\
export PATH=\$PATH:/full/path/to/DADDY\_ROOT/daddy}\\
\\
then save the file, open a new tarminal, and type \texttt{daddy.py -help} to check
if it works.\\
\\
\textbf{Setting \texttt{PATH} variable on Windows}

\begin{itemize}

\item Windows XP:
\begin{enumerate}
\item Start -> Control Panel -> System -> Advanced
\item Click on Environment Variables, under System Variables, find PATH, and click
	  on it.
\item In the Edit windows, modify PATH by adding the full path of
	  \texttt{DADDY\_ROOT/daddy} to the value for PATH (separate with a semicolon).
	  If you do not have the item PATH, you may select to add a new variable and
	  add PATH as the name and the location of the class as the value.
\item Close the window.
\item Reopen Command prompt window, and type \texttt{daddy.py -help} to check
	  if it works.
\end{enumerate}

\item Windows Vista:
\begin{enumerate}
\item Right click My Computer icon.
\item Choose Properties from the context menu.
\item Click Advanced tab (Advanced system settings link in Vista).
\item In the Edit windows, modify PATH by adding the full path of
	  \texttt{DADDY\_ROOT/daddy} to the value for PATH (separate with a semicolon).
	  If you do not have the item PATH, you may select to add a new variable and
	  add PATH as the name and the location of the class as the value.
\item Reopen Command prompt window, and type \texttt{daddy.py -help} to check
	  if it works.
\end{enumerate}

\item Windows 7:
\begin{enumerate}
\item Select Computer from the Start menu.
\item Choose System Properties from the context menu.
\item Click Advanced system settings -> Advanced tab.
\item Click on Environment Variables, under System Variables, find PATH, and click
	  on it.
\item In the Edit windows, modify PATH by adding the full path of
	  \texttt{DADDY\_ROOT/daddy} to the value for PATH (separate with a semicolon).
	  If you do not have the item PATH, you may select to add a new variable and
	  add PATH as the name and the location of the class as the value.
\item Reopen Command prompt window, and type \texttt{daddy.py -help} to check
	  if it works.
\end{enumerate}

\end{itemize}
\newpage

\section{I/O Formats}

\subsection{Input File Format}

For DADDY a system is a set of subsystems, where each subsystem is represented as
an LTS (Labelled Transition System). It uses the Aldebaran file format to describe
the LTSs. This is a very simple format to represent finite state machines, and is
also the format that \texttt{ltsgraph} understands. Remember the application uses
this tool for draw the subsystems; this is a nicer way to see and understand them.

\subsubsection{The Aldebaran file format}

The format consists of two types of lines. The first line of the file, called the
\emph{header}, contains general information about the system, it has the name of 
the initial state (it must be 0 for compatibility with the \emph{ltsgraph} tool),
the number of transitions and the number states the system has.\\ 

\texttt{header ::= des(init\_state, num\_trnsition, num\_states)}\\
\\
The remainder lines represent the system's transitions, they are called
\emph{aut\_edge}, and contain the \emph{source} and \emph{destination} states, and
the name of the \emph{event} that produce the transition. The \emph{event} name
must be a string enclosed in double quotes.\\

\texttt{aut\_edge ::=  (src\_state, event\_name, dest\_state)}\\
\\
The files with the Aldebaran format has \texttt{.aut} extension.
Here we show an example:\\
\\
\texttt{des(0,4,3)}\\
\texttt{(0,"start",1)}\\
\texttt{(1,"move\_forward",2)}\\
\texttt{(2,"move\_backeard",1)}\\
\texttt{(2,"finish",0)}

\subsubsection{Restrictions to the Aldebaran format}

DADDY adds some restrictions to the Aldebaran file format in order to effectively
model the systems it works with. These restrictions are related with the names of
the events.\\
\\
Before we give the restrictions, we are going to explain the systems with the
application works. DADDY assumes that a system is a set of subsystems working in
parallel, each subsystem is represented as an LTS. A Labelled Transition System
consists of a set of states, an initial state, a set of transitions, and an
alphabet. The alphabet is the set of system's event, i.e. the transition's label.
These events are separated in three groups: observable normal events, unobservable
normal events, and unobservable fault events. To distinguish between them, their
names must start with a special character.

\begin{itemize}
\item An observable normal event starts with the character \texttt{'o'}.
\item An unobservable normal event starts with the character \texttt{'u'}.
\item An unobservable fault event starts with the character \texttt{'f'}.
\end{itemize}%
%
So, even the Aldebaran format support any character string as transition label,
you must respect the above restrictions for the event names, otherwise DADDY will
not be able to parse the file correctly. Following, we show an example of an
Aldebaran file that can be parsed by DADDY:\\
\\
\texttt{des(0,4,3)}\\
\texttt{(0,"o1",1)}\\
\texttt{(1,"u1",2)}\\
\texttt{(2,"o2",1)}\\
\texttt{(2,"f1",0)}

\subsection{Output File Format}

In order to decide diagnosability, and depending on the mode you are running the
application, it does different operation on the subsystems. Most of those
operations generate new subsystems, which can be stored in a \texttt{.aut} file
and then be graphed. Almost all of those files are normal Aldebaran format plus
the restrictions from the preview section, but there are two types of them that
need special attention. These are the \textbf{Diagnoser} and the
\textbf{Twin-Plant}.

\subsubsection{The Diagnoser}

The Diagnoser of a system $S$, called $D(S)$, is a special system that contains
only observable events, and its states are tuples of the form $(q,F)$, where $q$
is a state from $S$, and $F$ is a the set of faults carried from the initial state
of $S$ to the state $q$.\\
\\
As any other system, the Diagnoser can be stored in a \texttt{.aut} file, but
there is a problem, the Aldebaran format doesn't allow to put information within
the state's name. So, we decide that then information of faults be saved into the
event name of the outgoing edges of the state.\\
\\
For example, if we have a Diagnoser with the next transition:\\

$((q_1,\{f_3,f_4\}),"o2",(q_2,\{f_3,f_4,f_5\}))$\\
\\
it will be stored as:\\

\texttt{(1,"o2\#(f3,f4)",2)}.

\subsubsection{The Twin-Plant}

The twin-plant of a system $S$, called $T(S)$, is another system created from the
composition of two diagnosers, i.e. $T(S) = D^l (S) || D^r (S)$. A state of a
twin-plant is of the form $((q^l,F^l),(q^r,F^r))$, where $(q^l,F^l)$ and
$(q^r,F^r)$ are states from $D^l (S)$ and $D^r (S)$ respectively.\\
\\
Like with the Diagnoser (see above), we can not stored a twin-pant state into an
Aldebaran state. As before, we put the information within the events name of the
outgoing edges of the twin-plant states.\\
\\
For example, if we have the following transition:\\

$(((q^l_1,\{f_1,f_2\}),(q^r_1,\emptyset)),$
$"o5",$
$((q^l_2,\{f_1,f_2,f_3\}),(q^r_1,\emptyset)))$\\
\\
it will be stored as:\\

\texttt{(1,"o5\#L(f1,f2)\#R()",2)}

%\subsection{Screen Output}
%\subsubsection{For Mode -m=0}
%\subsubsection{For Mode -m=1}
%\subsubsection{For Mode -m=2}

\newpage

\section{Command Line Arguments}

In this section we explain the command line arguments for each mode in which DADDY
can run.\\
\\
\textbf{Choosing Mode}

\begin{description}
	\item[\texttt{-m=0|1|2}] :

	This argument specify the mode in which the application will run. By default
	the mode is 0 (\texttt{-m=0}).
\end{description}%
%
\textbf{Common Arguments For All Modes}

\begin{description}
	\item[\texttt{-s=S1,...,Sn}] :

	List of subsystems. The names of the subsystems must be separated by a comma,
	and must no be empty space between them. Each name in the list corresponds to
	an Aldebaran file, with extension \texttt{.aut}. The file extension must not
	be included in the names on the list. If the file name contains empty spaces,
	it must be enclosed in double quotes. The next lien shows an example of a well
	formed list of subsystems.

	\texttt{-s=N1,"N 2",N3}

	\item[\texttt{-f=F1,...,Fm}] :

	The list of faults for which the system is analyze to be diagnosable or not.
	The names of the faults must be separated by a comma, and must no be empty
	spaces between them. Also, the names must no contain empty spaces in them and
	must start with character \texttt{'f'}. The next lien shows an example of a
	well formed list of faults.

	\texttt{-f=f1,f2,f3}

	\item[\texttt{-t}] : (optional)

	With this option, the application measures the time the analysis takes.

	\item[\texttt{-v}] : (optional)

	With this option, the program generate a more detailed screen output.
\end{description}%
%
\textbf{Specific Arguments For Mode} \texttt{-m=0}

\begin{description}
	\item[\texttt{-c=C1,...,Ck}] : (optional)

	The list of the observable events in which the subsystems are going to be
	synchronize (Synchronization Event Set). The names of the events must be
	separated by a comma, and must no be empty spaces between them. Also, the
	names must no contain empty spaces in them and must start with character
	\texttt{'o'}. If the argument is not specified, by default the empty set is
	taken as the synchronization event set. The next lien shows an example of
	a well formed list of synchronization events.

	\texttt{c=o1,o2,o3}	

	\item[\texttt{-h=n}] : (optional)

	This argument sets the composition heuristic level. It is a number between 0
	and 5. by default \texttt{-h=0}. In the Section~\ref{sec:algorithms_heuristics}
	there is an explanation of how these heuristics work.

	\item[\texttt{-g}] : (optional)

	This option makes the application graph the generated systems. Graphics will
	be generated only if the global system is non-diagnosable.
\end{description}

\newpage

\section{Algorithms}\label{sec:algorithms}

In this section we give a brief description about the functionality of the
different modes.

\subsection{Mode -m=0}

This mode try to analyze diagnosability by doing the fewest number of composition
as possible. It uses the \textbf{twin-plant} method to check diagnosability on
its subsystems, and it also provides to the user six different heuristics for doing
the composition.

\subsubsection{Heuristics}\label{sec:algorithms_heuristics}

\textbf{Random}\\

The simplest way of composition is by randomly choose the subsystems to be
compound. The application gives us two different way to do random composition.

\begin{enumerate}
\item The first one is to randomly choose two subsystems and compose them.
      (This is the default action).

      This option can be used by adding \texttt{-h=0} to the command line.

\item The second is to randomly group the subsystems in pairs, and then compose
      those pairs.

      This option can be used by adding \texttt{-h=1} to the command line.
\end{enumerate}%
%
\textbf{By Its Diagnosability}\\

The second type of heuristic is to compose the subsystems regarding its
diagnosability property. First, it separates the subsystems into two groups,
diagnosable and non-diagnosable; and then, for each group it composes pairs of
subsystems (the pairs are choose randomly).\\

This option can be used by adding \texttt{-h=2} to the command line.\\
\\
\textbf{By Its Shared Events}\\

The last type consists of compose the subsystems regarding if they share observable
events or not. The application provides us with three heuristics:

\begin{enumerate}
\item The first consists in compose pairs of subsystems that not share observable
      events. In the case this heuristic cannot compose any subsystems (because all
      of them share at least one observable events) the application switches to an
      heuristic that solves the problem (\texttt{-m=4} o \texttt{-m=5}).

      This option can be used by adding \texttt{-h=3} to the command line.

\item The second consists in compose pairs of subsystems that share a subset of
      its observable events. In the case this heuristic cannot compose any
      subsystem, the application switches to an heuristic that solves the problem
      (\texttt{-m=3} o \texttt{-m=5}).

      This option can be used by adding \texttt{-h=4} to the command line.

\item The third consists in compose pairs of subsystems that share all its
      observable events. In case this heuristic cannot compose any subsystem, the
      application switches to an heuristic that solves the problem (\texttt{-m=3}
      o \texttt{-m=4}).

      This option can be used by adding \texttt{-h=5} to the command line.
\end{enumerate}

\subsection{Mode -m=1}

This is the most efficient method for checking diagnosability with daddy. It
represents a really distributed way for checking diagnosability, and in the worst
case it works like \texttt{-m=2}.\\
\\
The key of this mode, is that before it applies the twin-plant method, it first
reduce the subsystems removing from them the parts that are not relevant to the
analysis. This make the application works with smaller subsystems, reducing the
cost of the analysis. Even more, each analysis can be done in parallel with the
others.\\
\\
\textbf{NOTE} that actually DADDY does not run these analysis in parallel, it does
them sequentially, but as each one is independent from the others it can show the
time as if executions were done in parallel.

\subsection{Mode -m=2}

The las mode is just the implementation of the \textbf{twin-plant} method in its
purest form. The application compose all the subsystems in same order that they
ware specified in the command line, then generate its twin-plant and analyze it.
The implementation of this mode is just for comparison purposes with the other
modes.

\end{document}
